Inference at * 1 1 1 1 
Iof proof for Lemma inv image ind a:



1. T : Type
2. r : TT
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. S
9. j : T
10. k:T. r(k,j)  (y:S. (f(y) = k)  P(y))
11. y : S
12. f(y) = j
  P(y) 

latex

 by ((% Establish inductive hypothesis % 
Assert y':S. r(f(y'),f(y))  P(y')) 
ACollapseTHEN (
ACIfLabL 
AC[`main`,OnHyps [12;10;9;8] Thin   % cleanup % 
AC;`assertion`,((RepD) 
ACollapseTHENA (
AC(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))])) 

latex

AC1: 

AC1: 13. y' : S
AC1: 14. r(f(y'),f(y))
AC1:   P(y')
AC2: 

AC2: 8. y : S
AC2: 9. y':S. r(f(y'),f(y))  P(y')
AC2:   P(y)
AC.

Definitions

t  T, P  Q, x:A. B(x), x(s1,s2),